es:ES, e, e':E. loc(e) = loc(e')  Id  ([e, e'] = nil  E List  (e' <loc e)) 

latex

Definitions	ES, t  T, x:A. B(x), E, loc(e), Id, Prop, (e <loc e'), [e, e'], P  Q, P  Q, P & Q, P  Q, ||as||, A, e  e' , P  Q, Dec(P), False, ij
Lemmas	length zero, decidable int equal, non neg length, length wf1, decidable es-locl, es-le-not-locl, es-interval-non-zero, es-interval wf, es-locl wf, Id wf, es-loc wf, es-E wf, event system wf